-
Edinburgh Day Three
Achieved:
- Decided what to say in Dream Talk*
- Gave up on critic and decided to see if we could get IsaPlanner to do what it should do after the critic happened. Got part way through implementing this, then got stuck on the need to use Middle-Out Reasoning (which means leaving blank bits in your proof and filling them in later) because MJo ( ( Read more... )
-
Edinburgh Day Two
Achieved:
- JG sent me a PDF of our note on proof specification languages: read but not digested.
- Asked LD about putting induction challenge problems into TPTP THF - LD agrees with my approach. LD tried to check type definitions in IsaPlanner for me: "unfortunately most of my systems are halfway between broken and working... which means they're ( Read more... )
-
Edinburgh Day One
Achieved:
- Volunteered to give a Dream Talk on Friday
- Printed out and read my papers on Program Slicing which I said I'd talk about in the Dream Talk
- Long talk with LD about proof specification languages and control rules. Sent him draft paper on control rules by myself MJa and MP.
To Do:
- Write an abstract to go with the title for my Dream Talk, ( Read more... )